sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
UNQUOTE1(cons1(X, Z)) → FCONS(unquote(X), unquote1(Z))
QUOTE1(n__cons(X, Z)) → ACTIVATE(X)
SEL(s(X), cons(Y, Z)) → ACTIVATE(Z)
UNQUOTE(01) → 01
UNQUOTE1(cons1(X, Z)) → UNQUOTE(X)
FIRST(0, Z) → NIL
FIRST1(s(X), cons(Y, Z)) → FIRST1(X, activate(Z))
QUOTE1(n__first(X, Z)) → FIRST1(activate(X), activate(Z))
ACTIVATE(n__s(X)) → ACTIVATE(X)
QUOTE1(n__cons(X, Z)) → QUOTE(activate(X))
QUOTE(n__sel(X, Z)) → ACTIVATE(X)
UNQUOTE(s1(X)) → UNQUOTE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
SEL1(s(X), cons(Y, Z)) → ACTIVATE(Z)
ACTIVATE(n__0) → 01
FIRST(s(X), cons(Y, Z)) → CONS(Y, n__first(X, activate(Z)))
QUOTE(n__sel(X, Z)) → SEL1(activate(X), activate(Z))
FROM(X) → CONS(X, n__from(n__s(X)))
ACTIVATE(n__sel(X1, X2)) → SEL(activate(X1), activate(X2))
ACTIVATE(n__from(X)) → FROM(activate(X))
UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)
SEL1(s(X), cons(Y, Z)) → SEL1(X, activate(Z))
SEL1(0, cons(X, Z)) → QUOTE(X)
QUOTE1(n__first(X, Z)) → ACTIVATE(X)
QUOTE1(n__cons(X, Z)) → QUOTE1(activate(Z))
QUOTE(n__s(X)) → QUOTE(activate(X))
ACTIVATE(n__sel(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__first(X1, X2)) → FIRST(activate(X1), activate(X2))
ACTIVATE(n__nil) → NIL
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__sel(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__cons(X1, X2)) → CONS(activate(X1), X2)
QUOTE1(n__cons(X, Z)) → ACTIVATE(Z)
ACTIVATE(n__first(X1, X2)) → ACTIVATE(X1)
UNQUOTE(s1(X)) → S(unquote(X))
FIRST1(s(X), cons(Y, Z)) → ACTIVATE(Z)
QUOTE(n__s(X)) → ACTIVATE(X)
FIRST1(s(X), cons(Y, Z)) → QUOTE(Y)
ACTIVATE(n__first(X1, X2)) → ACTIVATE(X2)
UNQUOTE1(nil1) → NIL
QUOTE(n__sel(X, Z)) → ACTIVATE(Z)
FIRST(s(X), cons(Y, Z)) → ACTIVATE(Z)
SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))
QUOTE1(n__first(X, Z)) → ACTIVATE(Z)
FCONS(X, Z) → CONS(X, Z)
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
UNQUOTE1(cons1(X, Z)) → FCONS(unquote(X), unquote1(Z))
QUOTE1(n__cons(X, Z)) → ACTIVATE(X)
SEL(s(X), cons(Y, Z)) → ACTIVATE(Z)
UNQUOTE(01) → 01
UNQUOTE1(cons1(X, Z)) → UNQUOTE(X)
FIRST(0, Z) → NIL
FIRST1(s(X), cons(Y, Z)) → FIRST1(X, activate(Z))
QUOTE1(n__first(X, Z)) → FIRST1(activate(X), activate(Z))
ACTIVATE(n__s(X)) → ACTIVATE(X)
QUOTE1(n__cons(X, Z)) → QUOTE(activate(X))
QUOTE(n__sel(X, Z)) → ACTIVATE(X)
UNQUOTE(s1(X)) → UNQUOTE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
SEL1(s(X), cons(Y, Z)) → ACTIVATE(Z)
ACTIVATE(n__0) → 01
FIRST(s(X), cons(Y, Z)) → CONS(Y, n__first(X, activate(Z)))
QUOTE(n__sel(X, Z)) → SEL1(activate(X), activate(Z))
FROM(X) → CONS(X, n__from(n__s(X)))
ACTIVATE(n__sel(X1, X2)) → SEL(activate(X1), activate(X2))
ACTIVATE(n__from(X)) → FROM(activate(X))
UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)
SEL1(s(X), cons(Y, Z)) → SEL1(X, activate(Z))
SEL1(0, cons(X, Z)) → QUOTE(X)
QUOTE1(n__first(X, Z)) → ACTIVATE(X)
QUOTE1(n__cons(X, Z)) → QUOTE1(activate(Z))
QUOTE(n__s(X)) → QUOTE(activate(X))
ACTIVATE(n__sel(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__first(X1, X2)) → FIRST(activate(X1), activate(X2))
ACTIVATE(n__nil) → NIL
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__sel(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__cons(X1, X2)) → CONS(activate(X1), X2)
QUOTE1(n__cons(X, Z)) → ACTIVATE(Z)
ACTIVATE(n__first(X1, X2)) → ACTIVATE(X1)
UNQUOTE(s1(X)) → S(unquote(X))
FIRST1(s(X), cons(Y, Z)) → ACTIVATE(Z)
QUOTE(n__s(X)) → ACTIVATE(X)
FIRST1(s(X), cons(Y, Z)) → QUOTE(Y)
ACTIVATE(n__first(X1, X2)) → ACTIVATE(X2)
UNQUOTE1(nil1) → NIL
QUOTE(n__sel(X, Z)) → ACTIVATE(Z)
FIRST(s(X), cons(Y, Z)) → ACTIVATE(Z)
SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))
QUOTE1(n__first(X, Z)) → ACTIVATE(Z)
FCONS(X, Z) → CONS(X, Z)
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
UNQUOTE(s1(X)) → UNQUOTE(X)
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
UNQUOTE(s1(X)) → UNQUOTE(X)
The value of delta used in the strict ordering is 4.
POL(s1(x1)) = 1 + (4)x_1
POL(UNQUOTE(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)
The value of delta used in the strict ordering is 4.
POL(cons1(x1, x2)) = 1 + (4)x_2
POL(UNQUOTE1(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
ACTIVATE(n__sel(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__first(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__first(X1, X2)) → FIRST(activate(X1), activate(X2))
SEL(s(X), cons(Y, Z)) → ACTIVATE(Z)
ACTIVATE(n__sel(X1, X2)) → SEL(activate(X1), activate(X2))
ACTIVATE(n__sel(X1, X2)) → ACTIVATE(X1)
SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))
FIRST(s(X), cons(Y, Z)) → ACTIVATE(Z)
ACTIVATE(n__first(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
QUOTE(n__s(X)) → QUOTE(activate(X))
QUOTE(n__sel(X, Z)) → SEL1(activate(X), activate(Z))
SEL1(s(X), cons(Y, Z)) → SEL1(X, activate(Z))
SEL1(0, cons(X, Z)) → QUOTE(X)
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
FIRST1(s(X), cons(Y, Z)) → FIRST1(X, activate(Z))
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FIRST1(s(X), cons(Y, Z)) → FIRST1(X, activate(Z))
The value of delta used in the strict ordering is 12.
POL(sel(x1, x2)) = 3 + (3)x_1 + (2)x_2
POL(n__first(x1, x2)) = 3 + x_1
POL(from(x1)) = 3 + (4)x_1
POL(n__sel(x1, x2)) = 3 + (3)x_1 + (3)x_2
POL(n__cons(x1, x2)) = 3 + (2)x_1 + (3)x_2
POL(activate(x1)) = 3
POL(n__s(x1)) = 3 + (3)x_1
POL(n__nil) = 0
POL(0) = 2
POL(first(x1, x2)) = 2
POL(cons(x1, x2)) = 3 + x_1
POL(FIRST1(x1, x2)) = (4)x_1
POL(n__from(x1)) = 2 + (2)x_1
POL(n__0) = 3
POL(s(x1)) = 3 + (4)x_1
POL(nil) = 4
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
QUOTE1(n__cons(X, Z)) → QUOTE1(activate(Z))
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X